$\forall$$T$:Type, ${\it eq}$:EqDecider($T$), ${\it es}$:ES, $x$:Id, $e$:E.
\\[0ex]@loc($e$)($x$:$T$) $\Rightarrow$ (lastchange($x$;$e$) $<$ $e$) $\Rightarrow$ (($x$ after lastchange($x$;$e$)) = ($x$ when $e$) $\in$ $T$)